$\forall$$i$:Id, ${\it TA}$:(Id$\rightarrow$Type), $M$:(IdLnk$\rightarrow$Id$\rightarrow$Type). w{-}kindtype(${\it TA}$;$M$;$i$) $\in$ Knd$\rightarrow$Type